\begin{tabbing}
$\forall$$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $x$:Id, $k$:Knd, $T$:Type, ${\it test}$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow\mathbb{B}$).
\\[0ex]($\neg$($\uparrow$$x$ $\in$ dom(${\it ds}$)))
\\[0ex]$\Rightarrow$ (($\uparrow$isrcv($k$)) $\Rightarrow$ ($i$ = destination(lnk($k$))))
\\[0ex]$\Rightarrow$ Normal($T$)
\\[0ex]$\Rightarrow$ Normal(${\it ds}$)
\\[0ex]$\Rightarrow$ \=R{-}base{-}recognize($i$;${\it ds}$;$x$;$k$;$T$;${\it test}$)\+
\\[0ex]$\Vdash$ ${\it es}$.\=(@$i$($x$:$\mathbb{B}$) \& (state@$i$ $\subseteq$r State(${\it ds}$)) \& (kindtype($i$;$k$) $\subseteq$r $T$))\+
\\[0ex]c$\wedge$ \=$\forall$$e$@$i$.\+
\\[0ex]($\uparrow$($x$ when $e$))
\\[0ex]$\Leftarrow\!\Rightarrow$ ($\exists$\=${\it e'}$:E\+
\\[0ex](((${\it e'}$ $<$loc $e$) \& kind(${\it e'}$) = $k$ $\in$ Knd)
\\[0ex]c$\wedge$ ($\uparrow$(${\it test}$((state when ${\it e'}$),val(${\it e'}$))))))
\-\-\-\-
\end{tabbing}